Nuprl Lemma : normal-es-dt
11,40
postcript
pdf
da
:fpf(Knd;
k
.Type),
l
:IdLnk. normal-da{i:l}(
da
)
normal-ds{i:l}(es-dt(
l
;
da
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
rcv(
l
,
tg
)
,
P
Q
,
b
,
fpf-all(
A
;
eq
;
f
;
x
,
v
.
P
(
x
;
v
))
,
normal-type{i:l}(
T
)
,
normal-da{i:l}(
da
)
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
Id
,
Type
,
es-dt(
l
;
da
)
,
fpf-ap(
f
;
eq
;
x
)
,
normal-ds{i:l}(
ds
)
,
IdLnk
,
Knd
,
fpf(
A
;
a
.
B
(
a
))
Lemmas
es-dt-dom
,
es-dt-ap
,
rcv
wf
origin
da:fpf(Knd; k.Type), l:IdLnk. normal-da{i:l}(da) 
normal-ds{i:l}(es-dt(l; da)) da:fpf(Knd; k.Type), l:IdLnk. normal-da{i:l}(da) normal-ds{i:l}(es-dt(l; da)) 
Tx:A. B(x) Q
b
B(x)
B(x)
Q
Q